Search for: All records

Many of today’s message-passing systems not only require messages to be exchanged in a certain order but also to happen at a certaintimeor within a certaintime window. Such correctness conditions are particularly prominent in Internet of Things (IoT) and real-time systems applications, which interface with hardware devices that come with inherent timing constraints. Verifying compliance of such systems with the intendedtimed protocolis challenged by theirheterogeneity—ruling out any verification method that relies on the system to be implemented in one common language, let alone in a high-level and typed programming language. To address this challenge, this paper contributes alogical relationto verify that its inhabitants (the applications and hardware devices to be proved correct) comply with the given timed protocol. To cater to the systems’ heterogeneity, the logical relation is entirelysemantic, lifting the requirement that its inhabitants are syntactically well-typed. A semantic approach enables two modes of use of the logical relation for program verification:(i)once-and-for-allverification of anarbitrarywell-typed application, given a type system, and(ii)per-instanceverification of a specific application / hardware device (foreign code). To facilitate mode(i), the paper develops a refinement type system for expressing timed message-passing protocols and proves that any well-typed program inhabits the logical relation (fundamental theorem). A type checker for the refinement type system has been implemented in Rust, using an SMT solver to check satisfiability of timing constraints. Then, the paper demonstrates both modes of use based on a small case study of a smart home system for monitoring air quality, consisting of a controller application and various environment sensors. 

We develop a session types based framework for implementing and validating rate-based message passing systems in Internet of Things (IoT) domains. To model the indefinite repetition present in many embedded and IoT systems, we introduce a timed process calculus with a periodic recursion primitive. This allows us to model rate-based computations and communications inherent to these application domains. We introduce a definition of rate based session types in a binary session types setting and a new compatibility relationship, which we call rate compatibility. Programs which type check enjoy the standard session types guarantees as well as rate error freedom --- meaning processes which exchanges messages do so at the same rate. Rate compatibility is defined through a new notion of type expansion, a relation that allows communication between processes of differing periods by synthesizing and checking a common superperiod type. We prove type preservation and rate error freedom for our system, and show a decidable method for type checking based on computing superperiods for a collection of processes. We implement a prototype of our type system including rate compatibility via an embedding into the native type system of Rust. We apply this framework to a range of examples from our target domain such as Android software sensors, wearable devices, and sound processing. 

Abstract In this paper, we introduce a tiered-priority scheme for a synchronous message-passing language with support for selective communication and first-class communication protocols. Crucially, our scheme allows higher priority threads to communicate with lower priority threads, providing the ability to express programs that would be rejected by classic priority mechanisms that disallow any (potentially) blocking interactions between threads of differing priorities. We formalize our scheme in a novel semantic framework featuring a collection of actions to represent possible communications. Utilizing our formalism, we prove several important and desirable properties of our priority scheme. We also provide a prototype implementation of our tiered-priority scheme capable of expressing Concurrent ML and built in the MLton SML compiler and runtime. We evaluate the viability of our implementation through three case studies: a prioritized buyer-seller protocol and predictable shutdown mechanisms in the Swerve web server and eXene windowing toolkit. Our experiments show that priority can be easily added to existing CML programs without degrading performance. Our system exhibits negligible overheads on more modest workloads. 

Visual SLAM systems are concurrent, performance-critical systems that respond to real-time environmental conditions and are frequently deployed on resource-constrained hardware. Previous SLAM frameworks have primarily focused on algorithmic advances and their systems core has largely remained unchanged. In turn, SLAM systems suffer from performance problems that could be alleviated with improved systems design. In this paper, we present a quantitative analysis of the systems challenges to building consistent, accurate, and robust SLAM systems in the face of concurrency, variable environmental conditions, and resource-constrained hardware. We identify three interconnected challenges on systems design --- timeliness, concurrency, and context awareness --- and clarify their effects on performance. 

A compiler’s optimizer operates over abstract syntax trees (ASTs), continuously applying rewrite rules to replace sub- trees of the AST with more efficient ones. Especially on large source repositories, even simply finding opportunities for a rewrite can be expensive, as optimizer traverses the AST naively. In this paper, we leverage the need to repeatedly find rewrites, and explore options for making the search faster through indexing and incremental view maintenance (IVM). Concretely, we consider bolt-on approaches that make use of embedded IVM systems like DBToaster, as well as two new approaches: Label-indexing and TreeToaster, an AST- specialized form of IVM. We integrate these approaches into an existing just-in-time data structure compiler and show experimentally that TreeToaster can significantly improve performance with minimal memory overheads. 

UAVs are deployed in various applications including disaster search-and-rescue, precision agriculture, law enforcement and first response. As UAV software systems grow more complex, the drawbacks of developing them in low-level languages become more pronounced. For example, the lack of memory safety in C implies poor isolation between the UAV autopilot and other concurrent tasks. As a result, the most crucial aspect of UAV reliability-timely control of the flight-could be adversely impacted by other tasks such as perception or planning. We introduce JCopter, an autopilot framework for UAVs developed in a managed language, i.e., a high-level language with built-in safe memory and timing management. Through detailed simulation as well as flight testing, we demonstrate how JCopter retains the timeliness of C-based autopilots while also providing the reliability of managed languages. 

Abstract There is a growing interest in leveraging functional programming languages in real-time and embedded contexts. Functional languages are appealing as many are strictly typed, amenable to formal methods, have limited mutation, and have simple but powerful concurrency control mechanisms. Although there have been many recent proposals for specialized domain-specific languages for embedded and real-time systems, there has been relatively little progress on adapting more general purpose functional languages for programming embedded and real-time systems. In this paper, we present our current work on leveraging Standard ML (SML) in the embedded and real-time domains. Specifically, we detail our experiences in modifying MLton, a whole-program optimizing compiler for SML, for use in such contexts. We focus primarily on the language runtime, reworking the threading subsystem, object model, and garbage collector. We provide preliminary results over a radar-based aircraft collision detector ported to SML.